Nuprl Definition : sendMinimalR 11,40

sendMinimalR{$a:ut2, $tg:ut2}
sendMinimalR(T; t; l; ds1; ds2; P; Q; d1; d2; f)
== ([weakSendDoApplyR{$a:ut2, $tg:ut2}
== ([weakSendDoApplyR(T; t; l; ds1; f o' mu'(s,n. (P(s,n)))); 

== ([weakSendDoApplyR{$a:ut2, $tg:ut2}
== ([weakSendDoApplyR(; 0; lnk-inv(l); ds2; mu'(s,n. (Q(s,n))))]) 
latex



clarification:

sendMinimalR{$a:ut2, $tg:ut2}
sendMinimalR(T; t; l; ds1; ds2; P; Q; d1; d2; f)
== ([weakSendDoApplyR{$a:ut2, $tg:ut2}
== ([weakSendDoApplyR(T; t; l; ds1; f o' mu'(State(ds1);s,n. (P(s,n));d1)) / 
== ([[weakSendDoApplyR{$a:ut2, $tg:ut2}
== ([[weakSendDoApplyR(; 0; lnk-inv(l); ds2; mu'(State(ds2);s,n. (Q(s,n));d2)) / 
== ([[[]]]) 
latex


Definitions(L), f o' g, [car / cdr], weakSendDoApplyR{$a:ut2, $tg:ut2}(T; t; l; ds; f), , #$n, lnk-inv(l), mu'(P), State(ds), x.A(x), b, f(a), []

origin